Quiz (Week 4)

1. Minimal Specifications
- 1.1. Question 1
- 1.2. Question 2
2. Data Invariants
- 2.1. Question 3
- 2.2. Question 4
3. More on Testing Properties

1 Minimal Specifications

1.1 Question 1

Let gcd :: Int -> Int -> Int denote the function that returns the greatest common divisors of its inputs. The gcd function satisfies the following list of properties for all nonnegative input numbers x and y:

p1 x y = gcd x y == gcd y x
p2 x = gcd x 0 == gcd x x
p3 x y = gcd x (x * y) == gcd x x
p4 x y = gcd x (gcd y x) == gcd x y
p5 x = gcd x 1 == gcd 1 1

However, running tests for all of these properties takes too long for the impatient programmer. This is because many of these properties are logically redundant. If property A logically implies property B, then testing for property B is unlikely to fail when testing for property A has already passed.

Choose a subset of the properties above that, together with the usual laws of arithmetic involving addition and multiplication, imply all of the others, but do not contain any redundant properties.

Hint: There are two approaches to this question. First, use equational reasoning to see if you can derive (say) p1 from p2-p5. If you succeed, you know that p1 is redundant.

You can also think about possible (not necessarily correct) implementations of gcd that would fail the above properties. If you cannot write an implementation that fails a given property but passes all of the others, it's a good indication that the property is redundant.

✗p3 alone,
✗p1 and p2,
✗p1, p2 and p3,
✔p1, p3 and p4,
✗p1, p3 and p5,
✗p1, p2, p3, p4 and p5.

Property 3 alone cannot imply all the others: the function f x y == x satisfies f x (x * y) == x == f x x, but clearly does not satisfy the analogue of property 1, f x y == f y x.

Properties 1, 2 and 3 cannot imply all the others: the function f x y = if even x && even y then 1 else 0 satisfies both f x y == f y x, f x 0 == f x x and f x (x * y) = f x x, but not f x (f y x) == f x y, because f 2 (f 1 2) == f 2 0 == 1, while f 2 1 == 0.

In the set of properties 1, 3 and 5, number 5 is redundant. We show this using equational reasoning.

  gcd x 1
== -- by p1
  gcd 1 x
== -- by arithmetic x == 1 * x
  gcd 1 (1 * x)
== -- by p3 with x := 1
  gcd 1 1

We already know properties 1 and 3 imply the 5th, but not the 4th, so all we need to verify is that properties 1, 3 and 4 imply the 2nd. Again, we can use equational reasoning

  gcd x 0
== -- by x * 0 == 0
  gcd x (x * 0)
== -- by p3 with y := 0
  gcd x x

1.2 Question 2

Here's a standard (inefficient) reverse function for lists, and a collection of QuickCheck properties to specify it.

rev :: [Int] -> [Int]
rev (x:xs) = rev xs ++ [x]
rev []     = []

prop_1 :: [Int] ->  Bool
prop_1 xs = length (rev xs) == length xs

prop_2 :: [Int] -> [Int] -> Bool
prop_2 xs ys = rev (xs ++ ys) == rev ys ++ rev xs

prop_3 :: [Int] -> Int -> Bool
prop_3 xs x = count x xs == count x (rev xs)
  where
    count x xs = length (filter (== x) xs)

Which of the above properties is redundant given the other two?

✔prop_1
✗prop_2
✗prop_3
✗None of the above.

Property 3 essentially says that the output of reverse is a permutation of its input. Given that, we already know that the lengths will be the same. Thus property 1 is redundant.

2 Data Invariants

We have decided to represent undirected graphs using adjacency matrices. For example, a graph of four nodes arranged in a rectangle:

0 ----- 1
|       |
|       |
2 ----- 3

Would be represented as the matrix:

type Graph = [[Bool]]

m :: Graph
m = [[False, True,  True,  False],
     [True,  False, False, True ],
     [True,  False, False, True ],
     [False, True,  True,  False]]

That is, the value (m !! a) !! b is True iff the node numbered a is connected to the node numbered b.

2.1 Question 3

Select all data invariants that should apply to our Graph type, assuming g :: Graph:

✔transpose g == g
✗all or g
✔all (\x -> length x == length g) g
✗map reverse g == g

In order to be an adjacency matrix, the number of rows and columns must be equal, hence property 3 is needed. To represent an undirected graph, the transpose of the matrix must be equal to the original matrix (it is diagonally symmetrical), hence property 1. The second property is meaningless and not true if you have a node disconnected from all others. The fourth property also holds for our example, but not in general (for example if node 1 is not connected to node 3).

2.2 Question 4

We have the following graph operations:

newGraph :: Int -- number of nodes
         -> Graph
newGraph n = replicate n (replicate n False)

connected :: Graph -> (Int, Int) -> Bool
connected g (x, y) | x < length g && y < length g = (g !! x) !! y 
                   | otherwise                    = False

connect :: (Int, Int) -> Graph -> Graph
connect (x, y) =
  modify y (modify x (\_ -> True)) .
  modify x (modify y (\_ -> True))
  where
    modify :: Int -> (a -> a) -> [a] -> [a]
    modify 0 f (x:xs) = f x : xs
    modify n f (x:xs) = x : modify (n - 1) f xs
    modify n f []     = []

We have defined a wellformedness predicate for our data invariants, called wellformed. Select the properties we should assert about our operations¹.

✔wellformed (newGraph n)
✗wellformed (connect x y g) ==> wellformed g
✗wellformed (connect x y g)
✔wellformed g ==> wellformed (connect x y g)

The third property does not necessarily apply, if the input graph is not well formed. The second property may apply in this case, but it is not necessary nor sufficient to show our data invariants are preserved.

The other properties states that outputs are wellformed when inputs are wellformed, which is correct.

3 More on Testing Properties

3.1 Question 5

Consider the gcd function from Question 1. Define the function

f :: Int -> Int
f = gcd 2

Which of the following testing strategies should we use to test f?

✗Invertibility
✗Involution
✔Idempotence

The operation f is not invertible, since f 2 == 2 and f 4 == 2. Thus, 1 cannot be used. Since being involutive is a special case of being invertible, 2 cannot be used either. However, f is clearly idempotent.

3.2 Question 6

Which subsets of the following properties uniquely specify that f computes the gcd function for all nonnegative integer inputs?

p1 x = f 0 x == x
p2 x y = f x y == f y x
p3 x y = x <= y ==> f x y == f x (y - x)
p4 x y = x <= y ==> f x y == f x (f x y)

✗p1 and p2,
✗p1 and p4,
✔p1, p2 and p3,
✗p1, p2 and p4

We show that p1, p2 and p3 uniquely specify gcd for. Assume that a function f satisfies these properties. Then it obeys the following definition:

f 0 x = x
f x y
  | x > y = f y x
  | otherwise = f x (y - x)

This definition allows us to calculate f for any nonnegative input value of x, y. This is because in every two recursive iterations, the difference between the two inputs decreases.

The other answers cannot be correct: e.g. the max function also satisfies all the other properties.

3.3 Question 7

The following code converts Haskell Int values to and from strings containing their hexadecimal representation (as sequences consisting only of the characters '0', '1', '2', '3', '4', '5', '6', '7', '8', '9', 'A', 'B', 'C', 'D', 'E', 'F').

toHex :: Int -> String
toHex 0 = ""
toHex n =
  let
    (d,r) = n `divMod` 16
  in
    toHex d ++ ["0123456789ABCDEF" !! r]

fromHex :: String -> Int
fromHex = fst . foldr eachChar (0,1)
  where
    eachChar c (sum, m) =
      case elemIndex (toUpper c) "0123456789ABCDEF" of
        Just i  -> (sum + i * m, m * 16)
        Nothing -> (sum        , m * 16)

Select all properties that these functions satisfy.

✔i >= 0 ==> fromHex (toHex i) == i,
✔i > 0 ==> length (toHex i) <= length (show i),
✗all (`elem` "0123456789") s ==> read s <= fromHex s,
✔all (`elem` "0123456789ABCDEF") s ==> fromHex s == fromHex ('0':s).

Property 1 is true as converting to a hexadecimal string and then back should result in the same number.

Property 2 is true, as for positive (i.e. nonzero) integers the toHex representation will never be longer than the decimal string representation.

Property 3 is false as read will throw an exception when given the empty list for s.

Property 4 is true, as adding leading zeroes to a hexadecimal number does not change its value.

3.4 Question 8

Consider the Trie data structure from Assignment 1, here equipped with a difference operation:

data Trie = Trie Bool [(Char,Trie)] deriving (Eq,Show)

difference :: Trie -> Trie -> Trie
difference (Trie b ts) (Trie b' ts') =
  Trie (b && not b') (concat (map entryDiff ts)) where
  entryDiff :: (Char,Trie) -> [(Char,Trie)]
  entryDiff (x,t) =
    case lookup x ts' of
      Nothing -> [(x,t)]
      Just t' -> dropEmpty (x,difference t t')
  dropEmpty :: (Char,Trie) -> [(Char,Trie)]
  dropEmpty (_,Trie False []) = []
  dropEmpty t = [t]

This is the Trie analogue of set difference. The idea is that difference t1 t2 should return a dictionary containing all the words in t1 that do not occur in t2.

Which of the following properties hold, assuming correct implementations of the other functions from the assignment spec? Assume that all tries under consideration are well-formed and minimal, and that union and intersection have been defined so as to maintain minimality.

✗difference t t == t
✔difference t t == empty
✗difference empty t == t
✔difference empty t == empty
✔difference t empty == t
✗difference t empty == empty
✔difference (union t t') t == difference t' t
✗difference (intersection t t') t == difference t' t

A Trie represents a set of words. By assuming well-formedness and minimality, we know that each (finite) set of words has a unique representation as a Trie.

Therefore, the laws that these Trie operations satisfy should be exactly the algebraic laws of sets, where \(\emptyset\) is empty, \(\cup\) is union, \(\cap\) is intersection, and \(\backslash\) is difference.

Footnotes:

: This is not the same as selecting the properties which are true. Which properties are necessary to maintain our data invariants?

Submission is already closed for this quiz. You can click here to check your submission (if any).